(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
*(@x, @y) → #mult(@x, @y)
+(@x, @y) → #add(@x, @y)
attach(@line, @m) → attach#1(@line, @m)
attach#1(::(@x, @xs), @m) → attach#2(@m, @x, @xs)
attach#1(nil, @m) → nil
attach#2(::(@l, @ls), @x, @xs) → ::(::(@x, @l), attach(@xs, @ls))
attach#2(nil, @x, @xs) → nil
lineMult(@l, @m2) → lineMult#1(@m2, @l)
lineMult#1(::(@x, @xs), @l) → ::(mult(@l, @x), lineMult(@l, @xs))
lineMult#1(nil, @l) → nil
m1(@x) → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil))
m2(@x) → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil)))
m3(@x) → ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil))
m4(@x) → ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil))))
makeBase(@m) → makeBase#1(@m)
makeBase#1(::(@l, @m')) → mkBase(@l)
makeBase#1(nil) → nil
matrixMult(@m1, @m2) → matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))
matrixMult'(@m1, @m2) → matrixMult'#1(@m1, @m2)
matrixMult'#1(::(@l, @ls), @m2) → ::(lineMult(@l, @m2), matrixMult'(@ls, @m2))
matrixMult'#1(nil, @m2) → nil
matrixMult3(@m1, @m2, @m3) → matrixMult(matrixMult(@m1, @m2), @m3)
matrixMultList(@acc, @mm) → matrixMultList#1(@mm, @acc)
matrixMultList#1(::(@m, @ms), @acc) → matrixMultList(matrixMult(@acc, @m), @ms)
matrixMultList#1(nil, @acc) → @acc
matrixMultOld(@m1, @m2) → matrixMult'(@m1, transpose(@m2))
mkBase(@m) → mkBase#1(@m)
mkBase#1(::(@l, @m')) → ::(nil, mkBase(@m'))
mkBase#1(nil) → nil
mult(@l1, @l2) → mult#1(@l1, @l2)
mult#1(::(@x, @xs), @l2) → mult#2(@l2, @x, @xs)
mult#1(nil, @l2) → #abs(#0)
mult#2(::(@y, @ys), @x, @xs) → +(*(@x, @y), mult(@xs, @ys))
mult#2(nil, @x, @xs) → #abs(#0)
split(@m) → split#1(@m)
split#1(::(@l, @ls)) → split#2(@l, @ls)
split#1(nil) → tuple#2(nil, nil)
split#2(::(@x, @xs), @ls) → split#3(split(@ls), @x, @xs)
split#2(nil, @ls) → tuple#2(nil, nil)
split#3(tuple#2(@ys, @m'), @x, @xs) → tuple#2(::(@x, @ys), ::(@xs, @m'))
transAcc(@m, @base) → transAcc#1(@m, @base)
transAcc#1(::(@l, @m'), @base) → attach(@l, transAcc(@m', @base))
transAcc#1(nil, @base) → @base
transpose(@m) → transpose#1(@m, @m)
transpose#1(::(@xs, @xss), @m) → transpose#2(split(@m))
transpose#1(nil, @m) → nil
transpose#2(tuple#2(@l, @m')) → transpose#3(@m', @l)
transpose#3(::(@y, @ys), @l) → ::(@l, transpose(::(@y, @ys)))
transpose#3(nil, @l) → nil
transpose'(@m) → transAcc(@m, makeBase(@m))
The (relative) TRS S consists of the following rules:
#add(#0, @y) → @y
#add(#neg(#s(#0)), @y) → #pred(@y)
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y))
#add(#pos(#s(#0)), @y) → #succ(@y)
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y))
#mult(#0, #0) → #0
#mult(#0, #neg(@y)) → #0
#mult(#0, #pos(@y)) → #0
#mult(#neg(@x), #0) → #0
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y))
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #0) → #0
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y))
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y))
#natmult(#0, @y) → #0
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y))
#pred(#0) → #neg(#s(#0))
#pred(#neg(#s(@x))) → #neg(#s(#s(@x)))
#pred(#pos(#s(#0))) → #0
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x))
#succ(#0) → #pos(#s(#0))
#succ(#neg(#s(#0))) → #0
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x))
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
attach(::(@x453639_5, @xs453640_5), ::(@l453764_5, @ls453765_5)) →+ ::(::(@x453639_5, @l453764_5), attach(@xs453640_5, @ls453765_5))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [@xs453640_5 / ::(@x453639_5, @xs453640_5), @ls453765_5 / ::(@l453764_5, @ls453765_5)].
The result substitution is [ ].
(2) BOUNDS(n^1, INF)